(declare-const zero Float32)
(assert (= zero (_ +zero 8 24)))
(declare-const one Float32)
(assert (= one ((_ to_fp 8 24) RNE 1.0)))
(declare-const low Float32)
(assert (= low ((_ to_fp 8 24) RNE 1.0)))
(declare-const high Float32)
(assert (= high ((_ to_fp 8 24) RNE 2.0)))
(declare-const x Float32)
(declare-const y Float32)
(declare-const z Float32)
(assert (and (fp.leq low x) (fp.leq x y) (fp.leq y high)))
(assert (and (fp.leq zero z) (fp.leq z one)))
(assert (and (fp.isNormal x) (fp.isNormal y) (fp.isNormal z)))
(declare-const sfma Float32)
(assert (= sfma (fp.fma RNE x y z)))
(declare-const dfma Float32)
(assert (= dfma ((_ to_fp 8 24) RNE (fp.fma RNE ((_ to_fp 15 113) RNE x) ((_ to_fp 15 113) RNE y) ((_ to_fp 15 113) RNE z)))))
(declare-const dma Float32)
(assert (= dma ((_ to_fp 8 24) RNE (fp.add RNE (fp.mul RNE ((_ to_fp 11 53) RNE x) ((_ to_fp 11 53) RNE y)) ((_ to_fp 11 53) RNE z)))))
(assert (not (= sfma dfma)))
(check-sat)
